(0) Obligation:
Clauses:
p(a, b).
p(b, c).
tc(X, X).
tc(X, Y) :- ','(p(X, Z), tc(Z, Y)).
Query: tc(g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
tcB(X1) :- tcA(X1).
tcC(a, X1) :- tcB(X1).
tcC(b, X1) :- tcA(X1).
tcC(a, X1) :- tcB(X1).
tcC(b, X1) :- tcA(X1).
Clauses:
tccA(c).
tccB(b).
tccB(X1) :- tccA(X1).
Afs:
tcC(x1, x2) = tcC(x1)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [DT09].
(4) Obligation:
Triples:
Clauses:
tccA(c).
tccB(b).
tccB(X1) :- tccA(X1).
Afs:
tcC(x1, x2) = tcC(x1)
(5) TPisEmptyProof (EQUIVALENT transformation)
There are no more dependency triples. Hence, the dependency triple problem trivially terminates.
(6) YES